1 /-
2 Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Zhouhang Zhou
5
6 Show that each Borel measurable function can be approximated,
7 both pointwise and in L¹ norm, by a sequence of simple functions.
8 -/
9
10 import measure_theory.l1_space
src └─────────────────────┘
11
12 noncomputable theory
13 open lattice set filter topological_space
14 open_locale classical topological_space
15
16 universes u v
17 variables {α : Type u} {β : Type v} {ι : Type*}
18
19 namespace measure_theory
20 open ennreal nat metric
21 open_locale measure_theory
22 variables [measure_space α] [normed_group β] [second_countable_topology β]
23
24 local infixr ` →ₛ `:25 := simple_func
25 lemma simple_func_sequence_tendsto {f : α → β} (hf : measurable f) :
26 ∃ (F : ℕ → (α →ₛ β)), ∀ x : α, tendsto (λ n, F n x) at_top (𝓝 (f x)) ∧
27 ∀ n, ∥F n x∥ ≤ ∥f x∥ + ∥f x∥ :=
28 -- enumerate a countable dense subset {e k} of β
29 let ⟨D, ⟨D_countable, D_dense⟩⟩ := separable_space.exists_countable_closure_eq_univ β in
30 let e := enumerate_countable D_countable 0 in
31 let E := range e in
32 have E_dense : closure E = univ :=
33 dense_of_subset_dense (subset_range_enumerate D_countable 0) D_dense,
34 let A' (N k : ℕ) : set α :=
35 f ⁻¹' (metric.ball (e k) (1 / (N+1 : ℝ)) \ metric.ball 0 (1 / (N+1 : ℝ))) in
36 let A N := disjointed (A' N) in
37 have is_measurable_A' : ∀ {N k}, is_measurable (A' N k) :=
38 λ N k, hf.preimage $ is_measurable.inter is_measurable_ball $ is_measurable.compl is_measurable_ball,
39 have is_measurable_A : ∀ {N k}, is_measurable (A N k) :=
40 λ N, is_measurable.disjointed $ λ k, is_measurable_A',
id └────────┘
src └────────┘
typ └────────┘
41 have A_subset_A' : ∀ {N k x}, x ∈ A N k → x ∈ A' N k := λ N k, inter_subset_left _ _,
id └───────────────┘
src └───────────────┘
typ └───────────────┘
42 have dist_ek_fx' : ∀ {x N k}, x ∈ A' N k → (dist (e k) (f x) < 1 / (N+1 : ℝ)) :=
id └──┘
src └──┘
typ └──┘
43 λ x N k, by { rw [dist_comm], simpa using (λ a b, a) },
src └──┘ ┴ └──────────┘ └────┘ └┘
typ └──┘ ┴ └──────────┘ └────┘ └┘
doc └──┘ ┴ └──────────┘ └────┘ └┘
txt └──┘ ┴ └──────────┘ └────┘ └┘
par └──┘ ┴ └──────────┘ └────┘ └┘
pid └┘ ┴ ┴└────┘ └────┘ ┴┴
44 have dist_ek_fx : ∀ {x N k}, x ∈ A N k → (dist (e k) (f x) < 1 / (N+1 : ℝ)) :=
id └──┘
src └──┘
typ └──┘
45 λ x N k h, dist_ek_fx' (A_subset_A' h),
46 have norm_fx' : ∀ {x N k}, x ∈ A' N k → (1 / (N+1 : ℝ)) ≤ ∥f x∥ := λ x N k, by simp [ball_0_eq],
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
47 have norm_fx : ∀ {x N k}, x ∈ A N k → (1 / (N+1 : ℝ)) ≤ ∥f x∥ := λ x N k h, norm_fx' (A_subset_A' h),
48 -- construct the desired sequence of simple functions
49 let M N x := nat.find_greatest (λ M, x ∈ ⋃ k ≤ N, (A M k)) N in
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
50 let k N x := nat.find_greatest (λ k, x ∈ A (M N x) k) N in
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
51 let F N x := if x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k then e (k N x) else 0 in
52 -- prove properties of the construction above
53 have k_unique : ∀ {M k k' x}, x ∈ A M k ∧ x ∈ A M k' → k = k' := λ M k k' x h,
54 begin
55 by_contradiction k_ne_k',
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
txt └──────────────────────┘
par └──────────────────────┘
pid └──────┘
56 have NE : (A M k ∩ A M k').nonempty, from ⟨x, h⟩,
src └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └───┘ └┘ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └───┘ └┘ ┴
doc └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └───┘ └┘ ┴
txt └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └───┘ └┘ ┴
par └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └───┘ └┘ ┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘┴ └───┘ └┘ ┴
57 have E : A M k ∩ A M k' = ∅ := disjoint_disjointed' k k' k_ne_k',
src └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
txt └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
par └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
58 exact NE.ne_empty E,
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
59 end,
60 have x_mem_Union_k : ∀ {N x}, (x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k) → x ∈ ⋃ k ≤ N, A (M N x) k :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
61 λ N x h,
id ┴ ┴ ┴
typ ┴ ┴ ┴
62 @nat.find_greatest_spec (λ M, x ∈ ⋃ k ≤ N, (A M k)) _ N (
id └────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └────────────────────┘ ┴ ┴ ┴
typ └────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴
63 let ⟨M, hM⟩ := mem_Union.1 (h) in
id └─┘ ┴ └┘ └───────┘┴ ┴
src └───────┘┴
typ └─┘ ┴ └┘ └───────┘┴ ┴
64 let ⟨hM₁, hM₂⟩ := mem_Union.1 hM in
id └─┘ └─┘ └─┘ └───────┘┴
src └───────┘┴
typ └─┘ └─┘ └─┘ └───────┘┴
65 ⟨M, ⟨hM₁, hM₂⟩⟩),
66 have x_mem_A : ∀ {N x}, (x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k) → x ∈ A (M N x) (k N x) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
67 λ N x h,
id ┴ ┴ ┴
typ ┴ ┴ ┴
68 @nat.find_greatest_spec (λ k, x ∈ A (M N x) k) _ N (
id └────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────────┘ ┴
typ └────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
69 let ⟨k, hk⟩ := mem_Union.1 (x_mem_Union_k h) in
id └─┘ ┴ └┘ └───────┘┴ └───────────┘ ┴
src └───────┘┴
typ └─┘ ┴ └┘ └───────┘┴ └───────────┘ ┴
70 let ⟨hk₁, hk₂⟩ := mem_Union.1 hk in
id └─┘ └─┘ └─┘ └───────┘┴
src └───────┘┴
typ └─┘ └─┘ └─┘ └───────┘┴
71 ⟨k, ⟨hk₁, hk₂⟩⟩),
72 have x_mem_A' : ∀ {N x}, (x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k) → x ∈ A' (M N x) (k N x) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
73 λ N x h, mem_of_subset_of_mem (inter_subset_left _ _) (x_mem_A h),
id ┴ ┴ ┴ └──────────────────┘ └───────────────┘ └─────┘ ┴
src └──────────────────┘ └───────────────┘
typ ┴ ┴ ┴ └──────────────────┘ └───────────────┘ └─────┘ ┴
74 -- prove that for all N, (F N) has finite range
75 have F_finite : ∀ {N}, finite (range (F N)) :=
id ┴ └────┘ └───┘ ┴ ┴
src └────┘ └───┘
typ ┴ └────┘ └───┘ ┴ ┴
doc └────┘ └───┘
76 begin
st └─────
77 assume N, apply finite_range_ite,
id └──────────────┘
src └──────┘ └────┘└──────────────┘
typ └──────┘ └────┘└──────────────┘
doc └──────┘ └────┘
txt └──────┘ └────┘
par └──────┘ └────┘
pid └──────┘ ┴
st ─────────┘└──────────────────────┘└─
78 { rw range_comp, apply finite_image, exact finite_range_find_greatest },
id └────────┘ └──────────┘ └────────────────────────┘
src └─┘└────────┘ └────┘└──────────┘ └────┘└────────────────────────┘┴
typ └─┘└────────┘ └────┘└──────────┘ └────┘└────────────────────────┘┴
doc └─┘ └────┘ └────┘ ┴
txt └─┘ └────┘ └────┘ ┴
par └─┘ └────┘ └────┘ ┴
pid ┴ ┴ ┴ ┴
st ───┘└───────────┘└──────────────────┘└─────────────────────────────────┘└┘└
79 { exact finite_range_const }
id └────────────────┘
src └────┘└────────────────┘┴
typ └────┘└────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────┘└─
80 end,
st ──┘
81 -- prove that for all N, (F N) is a measurable function
82 have F_measurable : ∀ {N}, measurable (F N) :=
id ┴ └────────┘ ┴ ┴
src └────────┘
typ ┴ └────────┘ ┴ ┴
doc └────────┘
83 begin
st └─────
84 assume N, refine measurable.if _ _ measurable_const,
id └───────────┘ └──────────────┘
src └──────┘ └─────┘└───────────┘└───┘└──────────────┘
typ └──────┘ └─────┘└───────────┘└───┘└──────────────┘
doc └──────┘ └─────┘ └───┘
txt └──────┘ └─────┘ └───┘
par └──────┘ └─────┘ └───┘
pid └──────┘ ┴ └───┘
st ─────────┘└─────────────────────────────────────────┘└─
85 -- show `is_measurable {a : α | a ∈ ⋃ (M : ℕ) (H : M ≤ N) (k : ℕ) (H : k ≤ N), A M k}`
st ─────────────────────────────────────────────────────────────────────────────────────────
86 { rw set_of_mem_eq, simp [is_measurable.Union, is_measurable.Union_Prop, is_measurable_A] },
id └───────────┘ └─────────────────┘ └──────────────────────┘
src └─┘└───────────┘ └────┘└─────────────────┘└┘└──────────────────────┘└┘ └┘
typ └─┘└───────────┘ └────┘└─────────────────┘└┘└──────────────────────┘└┘└─────────────┘└┘
doc └─┘ └────┘ └┘ └┘ └┘
txt └─┘ └────┘ └┘ └┘ └┘
par └─┘ └────┘ └┘ └┘ └┘
pid ┴ ┴┴ └┘ └┘ ┴┴
st ───┘└──────────────┘└──────────────────────────────────────────────────────────────────────┘└┘└
87 -- show `measurable (λ (x : α), e (k N x))`
st ──────────────────────────────────────────────
88 apply measurable.comp measurable_from_nat, apply measurable_find_greatest,
id └─────────────┘ └─────────────────┘ └──────────────────────┘
src └────┘└─────────────┘┴└─────────────────┘ └────┘└──────────────────────┘
typ └────┘└─────────────┘┴└─────────────────┘ └────┘└──────────────────────┘
doc └────┘ ┴ └────┘
txt └────┘ ┴ └────┘
par └────┘ ┴ └────┘
pid ┴ ┴ ┴
st ──────────────────────────────────────────┘└──────────────────────────────┘└─
89 assume k' k'_le_N, by_cases k'_eq_0 : k' = 0,
id └┘
src └───────────────┘ └───────┘ └─┘ ┴ └┘
typ └───────────────┘ └───────┘ └─┘└┘┴ └┘
doc └───────────────┘ └───────┘ └─┘ ┴ └┘
txt └───────────────┘ └───────┘ └─┘ ┴ └┘
par └───────────────┘ └───────┘ └─┘ ┴ └┘
pid └───────────────┘ ┴ └─┘ ┴ ┴┴
st ──────────────────┘└─────────────────────────┘└─
90 -- if k' = 0
st ───────────────
91 have : {x | k N x = 0} = (-⋃ (M : ℕ) (H : M ≤ N) (k : ℕ) (H : k ≤ N), A M k) ∪
id ┴ ┴ ┴┴ ┴ ┴ ┴
src └─────┘┴└──┘ ┴ ┴ ┴ └──┘ ┴ ┴┴└────┘ └─────┘ ┴┴┴ └─────┘ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴ └┘┴└
typ └─────┘┴└──┘┴┴ ┴ ┴ └──┘ ┴ ┴┴└────┘ └─────┘ ┴┴┴ └─────┘ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴ └┘┴└
doc └─────┘ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴└────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴ └┘ └
txt └─────┘ └──┘ ┴ ┴ ┴ └──┘ ┴ └────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
par └─────┘ └──┘ ┴ ┴ ┴ └──┘ ┴ └────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
pid └───┘└┘ └──┘ ┴ ┴ ┴ └──┘ ┴ └────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
st ─────────────────────────────────────────────────────────────────────────────────
92 (⋃ (m ≤ N), A m 0 - ⋃ m' (hmm' : m < m') (hm'N : m' ≤ N) (k ≤ N), A m' k),
id ┴ ┴ ┴ ┴ ┴
src ───────────────────┘ └────┘ ┴ ┴ ┴ └─┘┴┴ └──────────┘ ┴┴┴ └────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
typ ───────────────────┘ └────┘ ┴ ┴ ┴ └─┘┴┴ └──────────┘ ┴┴┴ └────────┘ ┴┴┴ └─────┘┴┴ ┴┴┴ ┴ ┴
doc ───────────────────┘ └────┘ ┴ ┴ ┴ └─┘ ┴ └──────────┘ ┴ ┴ └────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
txt ───────────────────┘ └────┘ ┴ ┴ ┴ └─┘ ┴ └──────────┘ ┴ ┴ └────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
par ───────────────────┘ └────┘ ┴ ┴ ┴ └─┘ ┴ └──────────┘ ┴ ┴ └────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
pid ───────────────────┘ └────┘ ┴ ┴ ┴ └─┘ ┴ └──────────┘ ┴ ┴ └────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─
93 { ext, split,
src └─┘ └───┘
typ └─┘ └───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
st ───┘└─┘└─────┘└─
94 { rw [mem_set_of_eq, mem_union_eq, or_iff_not_imp_left, mem_compl_eq, not_not_mem],
id └───────────┘ └──────────┘ └─────────────────┘ └──────────┘ └─────────┘
src └──┘└───────────┘└┘└──────────┘└┘└─────────────────┘└┘└──────────┘└┘└─────────┘┴
typ └──┘└───────────┘└┘└──────────┘└┘└─────────────────┘└┘└──────────┘└┘└─────────┘┴
doc └──┘ └┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ └┘ ┴
st ─────┘└───────────────┘└────────────┘└───────────────────┘└────────────┘└───────────┘└──
95 assume k_eq_0 x_mem,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └─────────────────┘
st ────────────────────────┘└─
96 simp only [not_exists, exists_prop, mem_Union, not_and, sub_eq_diff, mem_diff],
id └────────┘ └─────────┘ └───────┘ └─────┘ └─────────┘ └──────┘
src └─────────┘└────────┘└┘└─────────┘└┘└───────┘└┘└─────┘└┘└─────────┘└┘└──────┘┴
typ └─────────┘└────────┘└┘└─────────┘└┘└───────┘└┘└─────┘└┘└─────────┘└┘└──────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ ┴
st ───────────────────────────────────────────────────────────────────────────────────┘└─
97 refine ⟨M N x, ⟨nat.find_greatest_le, ⟨by { rw ← k_eq_0, exact x_mem_A x_mem} , _⟩⟩⟩,
id ┴ ┴ ┴ └──────────────────┘ └────┘ └─────┘ └───┘
src └─────┘ ┴ ┴ └┘ └──────────────────┘└┘ └─┘└───┘ └┘└────┘ ┴ └──────┘
typ └─────┘ ┴┴┴┴┴└┘ └──────────────────┘└┘ └─┘└───┘└────┘└──────┘└─────┘┴└───┘└──────┘
doc └─────┘ ┴ ┴ └┘ └┘ └─┘└───┘ └┘└────┘ ┴ └──────┘
txt └─────┘ ┴ ┴ └┘ └┘ └─┘└───┘ └┘└────┘ ┴ └──────┘
par └─────┘ ┴ ┴ └┘ └┘ └─┘└───┘ └──────┘ ┴ └──────┘
pid ┴ ┴ ┴ └┘ └┘ └──────┘ └──────┘ ┴ └──────┘
st ──────────────────────────────────────────────┘└────────────┘└───────────────────┘┴└─────┘└─
98 assume m hMm hmN k k_le_N,
src └───────────────────────┘
typ └───────────────────────┘
doc └───────────────────────┘
txt └───────────────────────┘
par └───────────────────────┘
pid └───────────────────────┘
st ──────────────────────────────┘└─
99 have := nat.find_greatest_is_greatest _ m ⟨hMm, hmN⟩,
id └───────────────────────────┘ ┴ └─┘ └─┘
src └──────┘└───────────────────────────┘└─┘ ┴ └┘ ┴
typ └──────┘└───────────────────────────┘└─┘┴┴ └─┘└┘└─┘┴
doc └──────┘ └─┘ ┴ └┘ ┴
txt └──────┘ └─┘ ┴ └┘ ┴
par └──────┘ └─┘ ┴ └┘ ┴
pid └───┘└─┘ └─┘ ┴ └┘ ┴
st ─────────────────────────────────────────────────────────┘└─
100 { simp only [not_exists, exists_prop, mem_Union, not_and] at this, exact this k k_le_N },
id └────────┘ └─────────┘ └───────┘ └─────┘ └──┘ ┴ └────┘
src └─────────┘└────────┘└┘└─────────┘└┘└───────┘└┘└─────┘└───────┘ └────┘ ┴ ┴ ┴
typ └─────────┘└────────┘└┘└─────────┘└┘└───────┘└┘└─────┘└───────┘ └────┘└──┘┴┴┴└────┘┴
doc └─────────┘ └┘ └┘ └┘ └───────┘ └────┘ ┴ ┴ ┴
txt └─────────┘ └┘ └┘ └┘ └───────┘ └────┘ ┴ ┴ ┴
par └─────────┘ └┘ └┘ └┘ └───────┘ └────┘ ┴ ┴ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴┴└─────┘ ┴ ┴ ┴ ┴
st ───────┘└─────────────────────────────────────────────────────────────┘└────────────────────┘└┘└
101 { exact ⟨M N x, ⟨nat.find_greatest_le, x_mem_Union_k x_mem⟩⟩ } },
id ┴ ┴ ┴ └──────────────────┘ └───────────┘ └───┘
src └────┘ ┴ ┴ └┘ └──────────────────┘└┘ ┴ └─┘
typ └────┘ ┴┴┴┴┴└┘ └──────────────────┘└┘└───────────┘┴└───┘└─┘
doc └────┘ ┴ ┴ └┘ └┘ ┴ └─┘
txt └────┘ ┴ ┴ └┘ └┘ ┴ └─┘
par └────┘ ┴ ┴ └┘ └┘ ┴ └─┘
pid ┴ ┴ ┴ └┘ └┘ ┴ └┘┴
st ──────────────────────────────────────────────────────────────────┘└──┘└
102 { simp only [mem_set_of_eq, mem_union_eq, mem_compl_eq],
id └───────────┘ └──────────┘ └──────────┘
src └─────────┘└───────────┘└┘└──────────┘└┘└──────────┘┴
typ └─────────┘└───────────┘└┘└──────────┘└┘└──────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────────────┘└─
103 by_cases x_mem : (x ∉ ⋃ (M : ℕ) (H : M ≤ N) (k : ℕ) (H : k ≤ N), A M k),
id ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴┴┴┴└────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴
typ └───────┘ └─┘ ┴┴┴┴┴└────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴┴┴┴┴┴┴ ┴ ┴
doc └───────┘ └─┘ ┴ ┴┴└────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ └────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ └────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ └────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────┘└─
104 { intro, apply find_greatest_eq_zero, assume k k_le_N hx,
id └───────────────────┘
src └───┘ └────┘└───────────────────┘ └────────────────┘
typ └───┘ └────┘└───────────────────┘ └────────────────┘
doc └───┘ └────┘ └────────────────┘
txt └───┘ └────┘ └────────────────┘
par └───┘ └────┘ └────────────────┘
pid ┴ └────────────────┘
st ───────┘└───┘└───────────────────────────┘└──────────────────┘└─
105 have : x ∈ ⋃ (M : ℕ) (H : M ≤ N) (k : ℕ) (H : k ≤ N), A M k,
id ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴┴└────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴
typ └─────┘┴┴ ┴┴└────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴┴┴┴┴┴┴ ┴
doc └─────┘ ┴ ┴┴└────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴
txt └─────┘ ┴ ┴ └────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ └────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ └────┘ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────┘┴└─────────────────────────────────────────────────┘└─
106 { rw [mem_Union], use M N x,
id └───────┘ ┴ ┴ ┴
src └──┘└───────┘┴ └──┘ ┴ ┴
typ └──┘└───────┘┴ └──┘┴┴┴┴┴
doc └──┘ ┴ └──┘ ┴ ┴
txt └──┘ ┴ └──┘ ┴ ┴
par └──┘ ┴ └──┘ ┴ ┴
pid └┘ ┴ ┴ ┴ ┴
st ───────────┘└───────────┘└──────────┘└─
107 rw mem_Union, use nat.find_greatest_le,
id └───────┘ └──────────────────┘
src └─┘└───────┘ └──┘└──────────────────┘
typ └─┘└───────┘ └──┘└──────────────────┘
doc └─┘ └──┘
txt └─┘ └──┘
par └─┘ └──┘
pid ┴ ┴
st ───────────────────────┘└────────────────────────┘└─
108 rw mem_Union, use k, rw mem_Union, use k_le_N, assumption },
id └───────┘ ┴ └───────┘ └────┘
src └─┘└───────┘ └──┘ └─┘└───────┘ └──┘ └─────────┘
typ └─┘└───────┘ └──┘┴ └─┘└───────┘ └──┘└────┘ └─────────┘
doc └─┘ └──┘ └─┘ └──┘ └─────────┘
txt └─┘ └──┘ └─┘ └──┘ └─────────┘
par └─┘ └──┘ └─┘ └──┘ └─────────┘
pid ┴ ┴ ┴ ┴ ┴
st ───────────────────────┘└─────┘└────────────┘└──────────┘└───────────┘└┘└
109 contradiction },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ─────────────────────┘└┘└
110 { rw not_not_mem at x_mem, assume h, cases h, contradiction,
id └─────────┘ ┴
src └─┘└─────────┘└───────┘ └──────┘ └────┘ └───────────┘
typ └─┘└─────────┘└───────┘ └──────┘ └────┘┴ └───────────┘
doc └─┘ └───────┘ └──────┘ └────┘ └───────────┘
txt └─┘ └───────┘ └──────┘ └────┘ └───────────┘
par └─┘ └───────┘ └──────┘ └────┘ └───────────┘
pid ┴ └───────┘ └──────┘ ┴
st ──────────────────────────────┘└────────┘└───────┘└─────────────┘└─
111 simp only [not_exists, exists_prop, mem_Union, not_and, sub_eq_diff, mem_diff] at h,
id └────────┘ └─────────┘ └───────┘ └─────┘ └─────────┘ └──────┘
src └─────────┘└────────┘└┘└─────────┘└┘└───────┘└┘└─────┘└┘└─────────┘└┘└──────┘└────┘
typ └─────────┘└────────┘└┘└─────────┘└┘└───────┘└┘└─────┘└┘└─────────┘└┘└──────┘└────┘
doc └─────────┘ └┘ └┘ └┘ └┘ └┘ └────┘
txt └─────────┘ └┘ └┘ └┘ └┘ └┘ └────┘
par └─────────┘ └┘ └┘ └┘ └┘ └┘ └────┘
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ ┴┴└──┘
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
112 rcases h with ⟨m, ⟨m_le_N, ⟨hx, hm⟩⟩⟩,
id ┴
src └─────┘ └───────────────────────────┘
typ └─────┘┴└───────────────────────────┘
doc └─────┘ └───────────────────────────┘
txt └─────┘ └───────────────────────────┘
par └─────┘ └───────────────────────────┘
pid ┴ └───────────────────────────┘
st ────────────────────────────────────────────┘└─
113 by_cases m_lt_M : m < M N x,
id ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴ ┴ ┴
typ └───────┘ └─┘┴┴ ┴┴┴┴┴┴
doc └───────┘ └─┘ ┴ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
114 { have := hm (M N x) m_lt_M nat.find_greatest_le (k N x) nat.find_greatest_le,
id └┘ ┴ └────┘ ┴ ┴ ┴ └──────────────────┘
src └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘└──────────────────┘
typ └──────┘└┘┴ ┴┴ ┴ └┘└────┘┴ ┴ ┴┴┴┴┴└┘└──────────────────┘
doc └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
txt └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid └───┘└─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
st ─────────┘└─────────────────────────────────────────────────────────────────────────┘└─
115 have := x_mem_A x_mem,
id └─────┘ └───┘
src └──────┘ ┴
typ └──────┘└─────┘┴└───┘
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ──────────────────────────────┘└─
116 contradiction },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───────────────────────┘└┘└
117 rw not_lt at m_lt_M, by_cases m_gt_M : m > M N x,
id └────┘ ┴ ┴ ┴ ┴ ┴
src └─┘└────┘└────────┘ └───────┘ └─┘ ┴┴┴ ┴ ┴
typ └─┘└────┘└────────┘ └───────┘ └─┘┴┴┴┴┴┴┴┴┴
doc └─┘ └────────┘ └───────┘ └─┘ ┴ ┴ ┴ ┴
txt └─┘ └────────┘ └───────┘ └─┘ ┴ ┴ ┴ ┴
par └─┘ └────────┘ └───────┘ └─┘ ┴ ┴ ┴ ┴
pid ┴ └────────┘ ┴ └─┘ ┴ ┴ ┴ ┴
st ──────────────────────────┘└───────────────────────────┘└─
118 { have := nat.find_greatest_is_greatest _ m ⟨m_gt_M, m_le_N⟩,
id └───────────────────────────┘ ┴ └────┘ └────┘
src └──────┘└───────────────────────────┘└─┘ ┴ └┘ ┴
typ └──────┘└───────────────────────────┘└─┘┴┴ └────┘└┘└────┘┴
doc └──────┘ └─┘ ┴ └┘ ┴
txt └──────┘ └─┘ ┴ └┘ ┴
par └──────┘ └─┘ ┴ └┘ ┴
pid └───┘└─┘ └─┘ ┴ └┘ ┴
st ─────────┘└────────────────────────────────────────────────────────┘└─
119 { have : x ∈ ⋃ k ≤ N, A m k,
id ┴ ┴ ┴┴ ┴ ┴
src └─────┘ ┴ ┴┴└───┘ ┴┴ ┴ ┴
typ └─────┘┴┴ ┴┴└───┘┴┴┴┴┴┴┴
doc └─────┘ ┴ ┴┴└───┘ ┴┴ ┴ ┴
txt └─────┘ ┴ ┴ └───┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ └───┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ └───┘ ┴ ┴ ┴
st ───────────┘└───────────────────────┘└─
120 { rw mem_Union, use 0, rw mem_Union, use nat.zero_le N, exact hx },
id └───────┘ └───────┘ ┴
src └─┘└───────┘ └───┘ └─┘└───────┘
typ └─┘└───────┘ └───┘ └─┘└───────┘ ┴
doc └─┘ └───┘ └─┘
txt └─┘ └───┘ └─┘
par └─┘ └───┘ └─┘
pid ┴ ┴┴ ┴
st ─────────────┘└──────────┘└─────┘└────────────┘┴ └┘
121 contradiction },
st └┘
122 { use m, split, exact m_le_N, rw mem_Union, use 0, rw mem_Union,
id ┴ └────┘
typ ┴ └────┘
123 use nat.zero_le _, exact hx } },
st └──┘
124 rw not_lt at m_gt_M, have M_eq_m := le_antisymm m_lt_M m_gt_M,
125 rw ← k'_eq_0, exact k_unique ⟨x_mem_A x_mem, by { rw [k'_eq_0, M_eq_m], exact hx }⟩ } } },
st └┘ └────┘
126 -- end of `have`
127 rw [k'_eq_0, this], apply is_measurable.union,
128 { apply is_measurable.compl,
129 simp [is_measurable.Union, is_measurable.Union_Prop, is_measurable_A] },
st └┘
130 { simp [is_measurable.Union, is_measurable.Union_Prop, is_measurable.diff, is_measurable_A] },
st └┘
131 -- if k' ≠ 0
132 have : {x | k N x = k'} = ⋃(m ≤ N), A m k' - ⋃m' (hmm' : m < m') (hm'N : m' ≤ N) (k ≤ N), A m' k,
id ┴ ┴ ┴ └┘ └┘ ┴ ┴
typ ┴ ┴ ┴ └┘ └┘ ┴ ┴
133 { ext, split,
134 { rw [mem_set_of_eq],
135 assume k_eq_k',
136 have x_mem : x ∈ ⋃ (M : ℕ) (H : M ≤ N) (k : ℕ) (H : k ≤ N), A M k,
id ┴ ┴ ┴
typ ┴ ┴ ┴
137 { have := find_greatest_of_ne_zero k_eq_k' k'_eq_0,
138 simp only [mem_Union], use M N x, use nat.find_greatest_le, use k', use k'_le_N,
id ┴ ┴ └┘
typ ┴ ┴ └┘
139 assumption },
st └┘
140 simp only [not_exists, exists_prop, mem_Union, not_and, sub_eq_diff, mem_diff],
141 refine ⟨M N x, ⟨nat.find_greatest_le, ⟨by { rw ← k_eq_k', exact x_mem_A x_mem} , _⟩⟩⟩,
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
142 assume m hMm hmN k k_le_N,
143 have := nat.find_greatest_is_greatest _ m ⟨hMm, hmN⟩,
id ┴ └─┘
typ ┴ └─┘
144 { simp only [not_exists, exists_prop, mem_Union, not_and] at this, exact this k k_le_N },
id ┴ └────┘
typ ┴ └────┘
st └┘
145 exact ⟨M N x, ⟨nat.find_greatest_le, x_mem_Union_k x_mem⟩⟩ },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
146 { simp only [mem_set_of_eq, mem_union_eq, mem_compl_eq], assume h,
147 have x_mem : x ∈ ⋃ (M : ℕ) (H : M ≤ N) (k : ℕ) (H : k ≤ N), A M k,
id ┴ ┴ ┴
typ ┴ ┴ ┴
148 { simp only [not_exists, exists_prop, mem_Union, not_and, sub_eq_diff, mem_diff] at h,
149 rcases h with ⟨m, ⟨hm, ⟨hx, _⟩⟩⟩,
150 simp only [mem_Union], use m, use hm, use k', use k'_le_N, assumption },
id ┴ └┘
typ ┴ └┘
st └┘
151 simp only [not_exists, exists_prop, mem_Union, not_and, sub_eq_diff, mem_diff] at h,
152 rcases h with ⟨m, ⟨m_le_N, ⟨hx, hm⟩⟩⟩,
153 by_cases m_lt_M : m < M N x,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
154 { have := hm (M N x) m_lt_M nat.find_greatest_le (k N x) nat.find_greatest_le,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
155 have := x_mem_A x_mem,
156 contradiction },
st └┘
157 rw not_lt at m_lt_M, by_cases m_gt_M : m > M N x,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
158 { have := nat.find_greatest_is_greatest _ m ⟨m_gt_M, m_le_N⟩,
id ┴ └────┘
typ ┴ └────┘
159 have : x ∈ ⋃ k ≤ N, A m k :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
160 by { rw mem_Union, use k', rw mem_Union, use k'_le_N, exact hx },
id └┘
typ └┘
st └┘
161 contradiction,
162 { use m, split, exact m_le_N, rw mem_Union, use k', rw mem_Union, use k'_le_N, exact hx }},
id ┴ └────┘ └┘
typ ┴ └────┘ └┘
st └─┘
163 rw not_lt at m_gt_M, have M_eq_m := le_antisymm m_lt_M m_gt_M,
164 exact k_unique ⟨x_mem_A x_mem, by { rw M_eq_m, exact hx }⟩ } },
st └┘ └──┘
165 -- end of `have`
166 rw this, simp [is_measurable.Union, is_measurable.Union_Prop, is_measurable.diff, is_measurable_A]
167 end,
st └─┘
168 -- start of proof
169 ⟨λ N, ⟨F N, λ x, measurable.preimage F_measurable is_measurable_singleton, F_finite⟩,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
170 -- The pointwise convergence part of the theorem
171 λ x, ⟨metric.tendsto_at_top.2 $ λ ε hε, classical.by_cases
id ┴ ┴
typ ┴ ┴
172 --first case : f x = 0
173 ( assume fx_eq_0 : f x = 0,
id ┴ ┴
typ ┴ ┴
174 have x_not_mem_A' : ∀ {M k}, x ∉ A' M k := λ M k,
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
175 begin
176 simp only [mem_preimage, fx_eq_0, metric.mem_ball, one_div_eq_inv, norm_zero,
177 not_and, not_lt, add_comm, not_le, dist_zero_right, mem_diff],
178 assume h, rw add_comm, exact inv_pos_of_nat
179 end,
st └─┘
180 have x_not_mem_A : ∀ {M k}, x ∉ A M k :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
181 by { assume M k h, have := disjointed_subset h, exact absurd this x_not_mem_A' },
st └┘
182 have F_eq_0 : ∀ {N}, F N x = 0 := λ N, by simp [F, if_neg, mem_Union, x_not_mem_A],
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
183 -- end of `have`
184 ⟨0, λ n hn, show dist (F n x) (f x) < ε, by {rw [fx_eq_0, F_eq_0, dist_self], exact hε}⟩ )
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st └┘
185 --second case : f x ≠ 0
186 ( assume fx_ne_0 : f x ≠ 0,
id ┴ ┴
typ ┴ ┴
187 let ⟨N₀, hN⟩ := exists_nat_one_div_lt (lt_min ((norm_pos_iff _).2 fx_ne_0) hε) in
id └┘
typ └┘
188 have norm_fx_gt : _ := (lt_min_iff.1 hN).1,
189 have ε_gt : _ := (lt_min_iff.1 hN).2,
190 have x_mem_Union_k_N₀ : x ∈ ⋃ k, A N₀ k :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
191 let ⟨k, hk⟩ := mem_closure_range_iff_nat.1 (by { rw E_dense, exact mem_univ (f x) }) N₀ in
id ┴ ┴
typ ┴ ┴
st └┘
192 begin
193 rw [Union_disjointed, mem_Union], use k,
id ┴
typ ┴
194 rw [mem_preimage], simp, rw [← one_div_eq_inv, add_comm],
195 exact ⟨hk , le_of_lt norm_fx_gt⟩
196 end,
st └─┘
197 let ⟨k₀, x_mem_A⟩ := mem_Union.1 x_mem_Union_k_N₀ in
id └┘
typ └┘
198 let n := max N₀ k₀ in
id ┴
typ ┴
199 have x_mem_Union_Union : ∀ {N} (hN : n ≤ N), x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k := assume N hN,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
200 mem_Union.2
201 ⟨N₀, mem_Union.2
202 ⟨le_trans (le_max_left _ _) hN, mem_Union.2
id └┘
typ └┘
203 ⟨k₀, mem_Union.2 ⟨le_trans (le_max_right _ _) hN, x_mem_A⟩⟩⟩⟩,
id └┘
typ └┘
204 have FN_eq : ∀ {N} (hN : n ≤ N), F N x = e (k N x) := assume N hN, if_pos $ x_mem_Union_Union hN,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
205 -- start of proof
206 ⟨n, assume N hN,
id ┴ ┴
typ ┴ ┴
207 have N₀_le_N : N₀ ≤ N := le_trans (le_max_left _ _) hN,
id ┴
typ ┴
208 have k₀_le_N : k₀ ≤ N := le_trans (le_max_right _ _) hN,
id ┴
typ ┴
209 show dist (F N x) (f x) < ε, from
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
210 calc
211 dist (F N x) (f x) = dist (e (k N x)) (f x) : by rw FN_eq hN
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
212 ... < 1 / ((M N x : ℝ) + 1) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
213 begin
214 have := x_mem_A' (x_mem_Union_Union hN),
215 rw [mem_preimage, mem_diff, metric.mem_ball, dist_comm] at this, exact this.1
216 end
st └─┘
217 ... ≤ 1 / ((N₀ : ℝ) + 1) :
id ┴
src ┴
typ ┴
218 @one_div_le_one_div_of_le _ _ ((N₀ : ℝ) + 1) ((M N x : ℝ) + 1) (nat.cast_add_one_pos N₀)
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
219 (add_le_add_right (nat.cast_le.2 (nat.le_find_greatest N₀_le_N
id └─────┘
typ └─────┘
220 begin rw mem_Union, use k₀, rw mem_Union, use k₀_le_N, exact x_mem_A end)) 1)
id └┘
typ └┘
st └─┘
221 ... < ε : ε_gt ⟩ ),
id ┴
typ ┴
222 -- second part of the theorem
223 assume N, show ∥F N x∥ ≤ ∥f x∥ + ∥f x∥, from
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
224 classical.by_cases
225 ( assume h : x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
226 calc
227 ∥F N x∥ = dist (F N x) 0 : by simp
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
228 ... = dist (e (k N x)) 0 : begin simp only [F], rw if_pos h end
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
st └─┘
229 ... ≤ dist (e (k N x)) (f x) + dist (f x) 0 : dist_triangle _ _ _
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
230 ... = dist (e (k N x)) (f x) + ∥f x∥ : by simp
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
231 ... ≤ 1 / ((M N x : ℝ) + 1) + ∥f x∥ :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
232 le_of_lt $ add_lt_add_right (dist_ek_fx (x_mem_A h)) _
233 ... ≤ ∥f x∥ + ∥f x∥ : add_le_add_right (norm_fx (x_mem_A h) ) _)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
234 ( assume h : x ∉ ⋃ M ≤ N, ⋃ k ≤ N, A M k,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
235 have F_eq_0 : F N x = 0 := if_neg h,
id ┴ ┴ ┴
typ ┴ ┴ ┴
236 by { simp only [F_eq_0, norm_zero], exact add_nonneg (norm_nonneg _) (norm_nonneg _) } )⟩⟩
st └┘
237
238 lemma simple_func_sequence_tendsto' {f : α → β} (hfm : measurable f)
id ┴ ┴ ┴
typ ┴ ┴ ┴
239 (hfi : integrable f) : ∃ (F : ℕ → (α →ₛ β)), (∀n, integrable (F n)) ∧
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
240 tendsto (λ n, ∫⁻ x, nndist (F n x) (f x)) at_top (𝓝 0) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
241 let ⟨F, hF⟩ := simple_func_sequence_tendsto hfm in
242 let G : ℕ → α → ennreal := λn x, nndist (F n x) (f x) in
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─────┘
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
243 let g : α → ennreal := λx, nnnorm (f x) + nnnorm (f x) + nnnorm (f x) in
id └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └┘
typ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘ └┘
244 have hF_meas : ∀ n, measurable (G n) := λ n, measurable.comp measurable_coe $
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
245 (F n).measurable.nndist hfm,
id ┴
typ ┴
246 have hg_meas : measurable g := measurable.comp measurable_coe $ measurable.add
id ┴
typ ┴
247 (measurable.add hfm.nnnorm hfm.nnnorm) hfm.nnnorm,
248 have h_bound : ∀ n, ∀ₘ x, G n x ≤ g x := λ n, all_ae_of_all $ λ x, coe_le_coe.2 $
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
249 calc
250 nndist (F n x) (f x) ≤ nndist (F n x) 0 + nndist 0 (f x) : nndist_triangle _ _ _
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
251 ... = nnnorm (F n x) + nnnorm (f x) : by simp [nndist_eq_nnnorm]
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
252 ... ≤ nnnorm (f x) + nnnorm (f x) + nnnorm (f x) : by { simp [nnreal.coe_le.symm, (hF x).2] },
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st └┘
253 have h_finite : lintegral g < ⊤ :=
id ┴
typ ┴
254 calc
255 (∫⁻ x, nnnorm (f x) + nnnorm (f x) + nnnorm (f x)) =
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
256 (∫⁻ x, nnnorm (f x)) + (∫⁻ x, nnnorm (f x)) + (∫⁻ x, nnnorm (f x)) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
257 by rw [lintegral_add, lintegral_add]; simp only [measurable.coe_nnnorm hfm, measurable.add]
258 ... < ⊤ : by { simp only [and_self, add_lt_top], exact hfi},
st └┘
259 have h_lim : ∀ₘ x, tendsto (λ n, G n x) at_top (𝓝 0) := all_ae_of_all $ λ x,
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
260 begin
261 apply (@tendsto_coe ℕ at_top (λ n, nndist (F n x) (f x)) 0).2,
id ┴ ┴ ┴
typ ┴ ┴ ┴
262 apply (@nnreal.tendsto_coe ℕ at_top (λ n, nndist (F n x) (f x)) 0).1,
id ┴ ┴ ┴
typ ┴ ┴ ┴
263 apply tendsto_iff_dist_tendsto_zero.1 (hF x).1
id ┴
typ ┴
264 end,
st └─┘
265 begin
266 use F, split,
267 { assume n, exact
268 calc
269 (∫⁻ a, nnnorm (F n a)) ≤ ∫⁻ a, nnnorm (f a) + nnnorm (f a) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
270 lintegral_le_lintegral _ _
271 (by { assume a, simp only [coe_add.symm, coe_le_coe], exact (hF a).2 n })
id ┴ ┴
typ ┴ ┴
st └┘
272 ... = (∫⁻ a, nnnorm (f a)) + (∫⁻ a, nnnorm (f a)) :
id ┴ ┴
typ ┴ ┴
273 lintegral_add (measurable.coe_nnnorm hfm) (measurable.coe_nnnorm hfm)
274 ... < ⊤ : by simp only [add_lt_top, and_self]; exact hfi },
st └┘
275 convert @tendsto_lintegral_of_dominated_convergence _ _ G (λ a, 0) g
id ┴ ┴ ┴
typ ┴ ┴ ┴
276 hF_meas h_bound h_finite h_lim,
277 simp only [lintegral_zero]
278 end
st └─┘
279
280 end measure_theory